predicate\_equivalent($T$;$P_{1}$;$P_{2}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$x$:$T$. ($P_{1}$($x$)) $\Leftarrow\!\Rightarrow$ ($P_{2}$($x$))